Inference at * 1 3 1 0 2 3 2 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
4. P(n)
  P(n) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term) 

latex

 .

Definitions

f(a), a < b, P  Q, x:A. B(x), , , x:AB(x)